Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • C cduce
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 18
    • Issues 18
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 3
    • Merge requests 3
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • cduce
  • cduce
  • Issues
  • #17

Closed
Open
Created Mar 01, 2017 by Tommaso Petrucciani@petruccianiDeveloper

Unsoundness with record typing

Functions on records can be given unsound types as in the following:

# let f = fun ({..} -> 'a) x -> x;;
val f : Record -> 'a = <fun>

# f {};;
- : 'a = { }

It seems that this 'a cannot be instantiated:

# (f {}) + 1;;
Characters 1-5:
This expression should have type:
!float | { .. } | Int
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
Atom & 'a

However, here it becomes unsound:

# f (f {});;
- : Empty = { }

Typing of field removal is also unsound:

# let g = fun ({a=Int;b=Bool;..}&'a -> {b=Bool;..}&'a) x -> x\a;;
val g : { a=Int b=Bool .. } & 'a -> { b=Bool .. } & 'a = <fun>

# g {a=2;b=`true};;
- : { a=2 b=`true } = { b=true }

# (g {a=2;b=`true}).a;;
- : 2 = true

# (g {a=2;b=`true}).b;;
- : `true = true

# (g {a=2;b=`true}).a + 2;;
File "runtime/value.ml", line 873, characters 9-15: Assertion failed
Assignee
Assign to
Time tracking