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 15
    • Issues 15
    • 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
  • #18

Closed
Open
Created Sep 18, 2017 by Tommaso Petrucciani@petruccianiDeveloper

Unsoundness with testing of function types

This code

(fun ((Int -> Int) -> `true; (Any \ (Int -> Int)) -> `false)
| ((Int -> Int) \ (Bool -> Bool)) -> `true
| (Int -> Int) & (Bool -> Bool) -> `true
| _ -> `false)
  (fun (x: Int): Int = x + 1)

breaks type preservation (in the cduce-next branch), producing

- : `true = false

The first function is well-typed; in particular, when the argument has type Int -> Int, the result must be true since either of the first two branches must apply (together, they cover Int -> Int entirely). The application is well-typed as well, but it reduces to the third branch (which is statically predicted to be unused) because the second function can be assigned neither type (Int -> Int) \ (Bool -> Bool) nor type (Int -> Int) & (Bool -> Bool).

This behaviour actually seems consistent with that described in the formalization (POPL '14 and '15), but it's unsound. When type tests are performed at runtime functions should probably be given negations of arrow types to ensure soundness. I'm not sure how this interacts with polymorphism though.

Assignee
Assign to
Time tracking