Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
  • This project
    • Loading...
  • Sign in / Register
C
cduce
  • Overview
    • Overview
    • Details
    • Activity
    • Cycle Analytics
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
  • Issues 18
    • Issues 18
    • List
    • Board
    • Labels
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Charts
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • cduce
  • cduce
  • Issues
  • #8

Closed
Open
Opened Mar 22, 2016 by Kim Nguyễn@kn 
  • Report abuse
  • New issue
Report abuse New issue

Type error in patricia trees

With the current commit 25b12781 patricia trees attached (see also [tests/poly/patricia.cd] in the distribution) [merge] function does not type. The error is

File "tests/poly/patricia.cd", line 69, characters 31-43:
This expression should have type:
Empty
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
'a & Int

The line at issue is

    | (<leaf key=k>x , t) ->   insert c k x t       

And the error message states that at the position of x was wating somethig of an empty type. Let us show why. First notice that

insert : ('a -> 'a -> 'a) -> Caml_int -> 'a -> Dict -> Leaf|Branch

since we have the following declaration

let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict): Leaf|Branch

First of all let us replace the line 69 with the following one:

    | (<leaf key=k>x , t) ->   insert   

we correctly obtain the following error:

File "tests/poly/patricia.cd", line 69, characters 31-37:
This expression should have type:
Branch | Leaf
but its inferred type is:
('_a_0 -> '_a_0 -> '_a_0) -> Caml_int -> '_a_0 -> [  ] | <brch bit=Caml_int
pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0 -> X2 where
X1 = [ X2 X2 ] and
X2 = <brch bit=Caml_int pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0
which is not a subtype, as shown by the sample:
('_a_0 -> '_a_0 -> '_a_0) -> Caml_int -> '_a_0 -> [  ] | <brch bit=Caml_int
pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0 -> X2 where
X1 = [ X2 X2 ] and
X2 = <brch bit=Caml_int pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0

Notice two things: the system expects as result of the matching something of type Leaf|Branch (perfect!) and the type deduced for @insert@ is exactly the original type where 'a has been renamed into a fresh variable. If now I use for this line the following definition

    | (<leaf key=k>x , t) ->   insert c  

I expect that the fresh variable '_a_0 is unified with 'a of the type of c, and thus that this expression has type Caml_int -> 'a -> Dict -> Leaf|Branch. Instead we obtain:

File "tests/poly/patricia.cd", line 69, characters 31-39:
This expression should have type:
Branch | Leaf
but its inferred type is:
Caml_int -> Arrow
which is not a subtype, as shown by the sample:
Caml_int -> Arrow

So what did happen? Well the fresh variable '_a_0 was WRONGLY substituted by Empty instead of by 'a. And therefore the deduced type is

Caml_int -> Empty -> Dict -> Leaf|Branch

(i.e. Caml_int -> Arrow). This explain why feeding two more arguments to it we obtain the error message that the function was expecting something of type Empty. Indeed with

    | (<leaf key=k>x , t) ->   insert c k x

we obtain

File "tests/poly/patricia.cd", line 69, characters 31-43:
This expression should have type:
Empty
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
'a & Int
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
No due date
2
Labels
Bug Typing
Assign labels
  • View labels
Reference: cduce/cduce#8